LEANGUARD: Lean-Verified Guardrails for Tool-Using Agents
LeanGuard：面向工具调用智能体的 Lean 验证护栏
🧭 LLM Agent 形式化护栏与自动修复 ★ 深度解读
Case Western Reserve University · UT Austin
在 LLM 智能体与工具之间嵌入 Lean 4 策略运行时，以形式化证明保证每次工具调用合规，并支持反馈或证明引导修复
📌 工作参考价值（4 点）
- 在电商导购/售后 Agent 的写操作（改订单、退款、发券）上，可借鉴“外部策略运行时 + 可信证据”架构：把业务规则写成 permits/requirements/forbids，所有工具调用先做 fail-closed 校验；关键点是不信 LLM 输出的文本，只信后端快照和监控日志，用户确认绑定到具体提案和状态版本，防止注入礼品卡/收款账户等越权操作。
- 将拒绝从“调用未执行”改为“失败规则 + 修复提示”，可减少重复试错并提高恢复率；论文中反馈使阻塞调用从 983 降到 719，恢复动作从 34 增至 48。售后场景可返回具体缺失条件（如需先读订单、需用户确认）而非笼统拒绝。
- 证明引导修复对参数值类违规很实用：当金额超预算、支付方式不合规、选错券时，可在规则引擎中预计算最近合规参数并随拒绝返回，或直接替换；论文在 252 个参数值拒绝中证明修复 88 个，中位 2ms，表明部分修复不必让模型重试。
- 若业务涉及支付、退款、隐私等强保障环节，可考虑用可验证语言编写核心策略，并检查证明无 sorry/非标准公理；但维护成本高，适合核心高风险写操作而非全量策略。